Example 1 in [Lucas - RTA'04]

Summary: Ex1_Luc04b

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas' transformation
  2. Zantema's transformation
  3. Ferreira and Ribeiro's transformation
• Positive results:
  1. Polynomial interpretation (MU-TERM)
  2. Giesl and Middeldorp's transformation (DPs + Polynomials @ MU-TERM)
  3. CSDP
  4. CSRPO

CS-TRS Ex1_Luc04b (file Ex1_Luc04b.csr)

Functions:  0 s nil cons nats pairs odds incr head tail

Constructors:  0 s nil cons

Variables:  X XS

Arities: 

ar(0) = 0
ar(s) = 1
ar(nil) = 0
ar(cons) = 2
ar(nats) = 0
ar(pairs) = 0
ar(odds) = 0
ar(incr) = 1
ar(head) = 1
ar(tail) = 1

Replacement map: 

µ(0) = {}
µ(s) = {1}
µ(nil) = {}
µ(cons) = {1}
µ(nats) = {}
µ(pairs) = {}
µ(odds) = {}
µ(incr) = {1}
µ(head) = {1}
µ(tail) = {1}

Rules:   (file Ex1_Luc04b)

nats -> cons(0,incr(nats))
pairs -> cons(0,incr(odds))
odds -> incr(pairs)
incr(cons(X,XS)) -> cons(s(X),incr(XS))
head(cons(X,XS)) -> X
tail(cons(X,XS)) -> XS

The CS-TRS in OBJ format (file Ex1_Luc04b.obj):

obj Ex1_Luc04b is
  sort S .
  op 0 : -> S .
  op s : S -> S .
  op nil : -> S .
  op cons : S S -> S [strat (1 0)] .
  op nats : -> S .
  op pairs : -> S .
  op odds : -> S .
  op incr : S -> S .
  op head : S -> S .
  op tail : S -> S .
  vars X XS : S .
  eq nats = cons(0,incr(nats)) .
  eq pairs = cons(0,incr(odds)) .
  eq odds = incr(pairs) .
  eq incr(cons(X,XS)) = cons(s(X),incr(XS)) .
  eq head(cons(X,XS)) = X .
  eq tail(cons(X,XS)) = XS .
endo

Negative results

1. The µ-termination of Ex1_Luc04b cannot be proved terminating by using Lucas' transformation. The TRS Ex1_Luc04b_L:

   nats -> cons(0)
   pairs -> cons(0)
   odds -> incr(pairs)
   incr(cons(X)) -> cons(s(X))
   head(cons(X)) -> X
   tail(cons(X)) -> XS
       

   contains extra variables.
2. The µ-termination of Ex1_Luc04b cannot be proved terminating by using Zantema's transformation. The TRS Ex1_Luc04b_Z:

   nats -> cons(0,n__incr(nats))
   pairs -> cons(0,n__incr(odds))
   odds -> incr(pairs)
   incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS)))
   head(cons(X,XS)) -> X
   tail(cons(X,XS)) -> activate(XS)
   incr(X) -> n__incr(X)
   activate(n__incr(X)) -> incr(X)
   activate(X) -> X
       

   is not terminating (due to the first rule).
3. The µ-termination of Ex1_Luc04b cannot be proved terminating by using Ferreira and Ribeiro's transformation. The TRS Ex1_Luc04b_FR:

   nats -> cons(0,n__incr(n__nats))
   pairs -> cons(0,n__incr(n__odds))
   odds -> incr(pairs)
   incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS)))
   head(cons(X,XS)) -> X
   tail(cons(X,XS)) -> activate(XS)
   incr(X) -> n__incr(X)
   nats -> n__nats
   odds -> n__odds
   activate(n__incr(X)) -> incr(activate(X))
   activate(n__nats) -> nats
   activate(n__odds) -> odds
   activate(X) -> X
       

   is not terminating:

   odds -> incr(pairs)
      -> incr(cons(0,n__incr(n__odds)))
      -> cons(s(0),n__incr(activate(n__incr(n__odds))))
      -> cons(s(0),n__incr(incr(activate(n__odds))))
      -> cons(s(0),n__incr(incr(odds)))
      -> ...
      

Positive results

1. The µ-termination of Ex1_Luc04b is proved in [Luc04b, Figure 2] by using the following polynomial interpretation (computed by MU-TERM):

   [0] = 0
   [s](X) = X
   [nil] = 0
   [cons](X1,X2) = X1 + 1/5.X2
   [nats] = 1
   [pairs] = 1
   [odds] = 3
   [incr](X) = X + 1
   [head](X) = X + 1
   [tail](X) = 5.X + 1
      

2. The µ-termination of Ex1_Luc04b is proved in [Luc04b, Figure 4] by using Giesl and Middeldorp's transformation. The TRS Ex1_Luc04b_GM:

   a__nats -> cons(0,incr(nats))
   a__pairs -> cons(0,incr(odds))
   a__odds -> a__incr(a__pairs)
   a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
   a__head(cons(X,XS)) -> mark(X)
   a__tail(cons(X,XS)) -> mark(XS)
   mark(nats) -> a__nats
   mark(pairs) -> a__pairs
   mark(odds) -> a__odds
   mark(incr(X)) -> a__incr(mark(X))
   mark(head(X)) -> a__head(mark(X))
   mark(tail(X)) -> a__tail(mark(X))
   mark(0) -> 0
   mark(s(X)) -> s(mark(X))
   mark(nil) -> nil
   mark(cons(X1,X2)) -> cons(mark(X1),X2)
   a__nats -> nats
   a__pairs -> pairs
   a__odds -> odds
   a__incr(X) -> incr(X)
   a__head(X) -> head(X)
   a__tail(X) -> tail(X)
   

   can be proved terminating by using the dependency pairs technique together with a polynomial interpretation over the rationals (use MU-TERM).
3. The µ-termination of Ex1_Luc04b can also be proved by using CSDP (computed by MuTerm).
4. The µ-termination of Ex1_Luc04b can also be proved by using CSRPO (computed by MuTerm).